rng_chom_p(r;s;f) == rng_hom_p(r;s;f) & (
a, b:|r|. ((f(a)) * (f(b))) = ((f(b)) * (f(a))))
clarification:
compound
rng_chom_p(r;s;f)
== rng_hom_p(r;s;f) & (
a:|r|, b:|r|. ((f(a)) (*s) (f(b))) = ((f(b)) (*s) (f(a))) 
|s|) | 13,42 |
a, b:|r|. ((f(a)) * (f(b))) = ((f(b)) * (f(a))))
a:|r|, b:|r|. ((f(a)) (*s) (f(b))) = ((f(b)) (*s) (f(a))) |s|)
| Up | |
| Wellformedness Lemmas | |
| Definitions | x:A. B(x) |